import Mathlib.Data.Finset.Basic
import Mathlib.Tactic

namespace CNVS

universe u v w

/-- Stato CNVS astratto: elementi validi e relazione direzionale. -/
structure CNVSState (Elem : Type u) where
  E : Set Elem
  R : Elem → Elem → Prop

/--
Modulo assiomatico minimale CNVS.
-/
structure CNVSAxioms
    (Elem : Type u)
    (TypeTag : Type v)
    (Verifier : Type w) where

  S : CNVSState Elem

  typeOf : Elem → TypeTag
  VLocal : Elem → Prop
  VGlobal : CNVSState Elem → Prop

  ConsistentR : CNVSState Elem → Prop
  Invariant : CNVSState Elem → Prop

  D : Elem → Finset Elem
  Rec : Finset Elem → Elem
  Assign : Elem → Verifier

  infoSize : Elem → Nat

  axiom_I_verified_existence :
    ∀ s : Elem, s ∈ S.E → VLocal s

  axiom_I_strong_local_form :
    ∀ s : Elem, s ∈ S.E ↔ VLocal s

  axiom_II_nonempty_decomposition :
    ∀ s : Elem, s ∈ S.E → (D s).Nonempty

  axiom_II_type_preservation :
    ∀ s f : Elem,
      s ∈ S.E →
      f ∈ D s →
      typeOf f = typeOf s

  axiom_II_non_uniformity :
    ∀ s : Elem,
      s ∈ S.E →
        ∃ fa fb : Elem,
          fa ∈ D s ∧
          fb ∈ D s ∧
          infoSize fa ≠ infoSize fb

  axiom_II_reconstruction :
    ∀ s : Elem, s ∈ S.E → Rec (D s) = s

  axiom_III_structural_global_validity :
    VGlobal S ↔
      (∀ s : Elem, s ∈ S.E → VLocal s) ∧
      ConsistentR S ∧
      Invariant S

  axiom_III_non_reducibility_witness :
    ∃ Sbad : CNVSState Elem,
      (∀ s : Elem, s ∈ Sbad.E → VLocal s) ∧
      ¬ VGlobal Sbad

namespace ConsistencyTest

abbrev Elem := Fin 3
abbrev TypeTag := Unit
abbrev Verifier := Unit

def testState : CNVSState Elem where
  E := {s | s = 0}
  R := fun a b => a = 0 ∧ b = 0

def testTypeOf : Elem → TypeTag :=
  fun _ => ()

def testVLocal : Elem → Prop :=
  fun s => s = 0

def testConsistentR : CNVSState Elem → Prop :=
  fun S => S.R 0 0

def testInvariant : CNVSState Elem → Prop :=
  fun _ => True

def testVGlobal : CNVSState Elem → Prop :=
  fun S =>
    (∀ s : Elem, s ∈ S.E → testVLocal s) ∧
    testConsistentR S ∧
    testInvariant S

def testD : Elem → Finset Elem :=
  fun s =>
    if s = 0 then
      ({1, 2} : Finset Elem)
    else
      ({s} : Finset Elem)

def testRec : Finset Elem → Elem :=
  fun _ => 0

def testAssign : Elem → Verifier :=
  fun _ => ()

def testInfoSize : Elem → Nat :=
  fun s =>
    if s = 1 then 1
    else if s = 2 then 2
    else 0

/--
Questo è il test di non-contraddizione.

Lean costruisce un modello concreto degli assiomi CNVS.
Se questo compila senza errori e senza `sorry`, gli assiomi sono soddisfacibili.
-/
def ExampleModel : CNVSAxioms Elem TypeTag Verifier where
  S := testState

  typeOf := testTypeOf
  VLocal := testVLocal
  VGlobal := testVGlobal

  ConsistentR := testConsistentR
  Invariant := testInvariant

  D := testD
  Rec := testRec
  Assign := testAssign

  infoSize := testInfoSize

  axiom_I_verified_existence := by
    intro s hs
    exact hs

  axiom_I_strong_local_form := by
    intro s
    rfl

  axiom_II_nonempty_decomposition := by
    intro s hs
    have h0 : s = 0 := hs
    simp [testD, h0]

  axiom_II_type_preservation := by
    intro s f hs hf
    simp [testTypeOf]

  axiom_II_non_uniformity := by
    intro s hs
    have h0 : s = 0 := hs
    refine ⟨1, 2, ?_, ?_, ?_⟩
    · simp [testD, h0]
    · simp [testD, h0]
    · simp [testInfoSize]

  axiom_II_reconstruction := by
    intro s hs
    have h0 : s = 0 := hs
    simp [testRec, h0]

  axiom_III_structural_global_validity := by
    rfl

  axiom_III_non_reducibility_witness := by
    let Sbad : CNVSState Elem :=
      { E := {s | s = 0}
        R := fun _ _ => False }
    refine ⟨Sbad, ?_, ?_⟩
    · intro s hs
      exact hs
    · intro h
      exact h.2.1
end ConsistencyTest

end CNVS